interleaving_occurence(T;L1;L2;L;f1;f2)
== ||L|| = ||L1||+||L2||
== & increasing(f1;||L1||) & (j:||L1||. L1[j] = L[f1(j)])
== & increasing(f2;||L2||) & (j:||L2||. L2[j] = L[f2(j)])
== & (j1:||L1||, j2:||L2||. f1(j1) = f2(j2)) 

latex

---

clarification:

interleaving_occurence(T;L1;L2;L;f1;f2)
== ||L|| = ||L1||+||L2||  
== & increasing(f1;||L1||) & (j:{0..||L1||}. L1[j] = L[f1(j)]  T)
== & increasing(f2;||L2||) & (j:{0..||L2||}. L2[j] = L[f2(j)]  T)
== & (j1:{0..||L1||}, j2:{0..||L2||}. f1(j1) = f2(j2)  ) 

latex

Definitions	, P & Q, increasing(f;k), l[i], x:A. B(x), {i..j}, ||as||, A
FDL editor aliases	interleaving_occurence